Nuprl Lemma : p-fun-exp_wf
11,40
postcript
pdf
A
:Type,
f
:(
A
(
A
+ Top)),
n
:
.
f
^
n
A
(
A
+ Top)
latex
ProofTree
Definitions
Type
,
t
T
,
Top
,
left
+
right
,
x
:
A
B
(
x
)
,
,
{
x
:
A
|
B
(
x
)}
,
x
:
A
.
B
(
x
)
,
#$n
,
{
i
..
j
}
,
f
o
g
,
x
.
A
(
x
)
,
p-id()
,
primrec(
n
;
b
;
c
)
,
f
^
n
Lemmas
primrec
wf
,
p-id
wf
,
p-compose
wf
,
int
seg
wf
,
nat
wf
,
top
wf
origin
A:Type, f:(A
(A + Top)), n:
. f^n 
A(A + Top)
A:Type, f:(A(A + Top)), n:. f^n A(A + Top)
TB(x)x:A. B(x)
}
x.A(x)